CHOICE-STRATEGY-IS: 
UNIT∧EQUALITY[=;3];

EDIT-STRATEGY-IS: 
DEPTH[5]∨LENGTH[4]∨SELDEPTH[F11,3];

ELAPSED-TIME =314168

NIL 1 2
1 F11(A13,F11(THM7,A25(F32(THM7,A13),A14)))= A26(F32(THM7,A13),A14);3 4
2 B(W)⊃A(F11(A13,W));5 14
3 R(F32(THM7,A13),A25(F32(THM7,A13),A14),W)⊃A26(F32(THM7,A13),A14)= W;7 8
4 R(F32(THM7,A13),W,F11(A13,F11(THM7,W)));9 14
5 B(X)∧R(A13,X,W)⊃A(W);A1
7 R(F32(THM7,A13),A25(F32(THM7,A13),A14),A26(F32(THM7,A13),A14));11 12
8 R(Y,Z,X)∧R(Y,Z,W)⊃W = X;F2
9 R(A13,F11(THM7,W),X)⊃R(F32(THM7,A13),W,X);13 14
11 A(A14);A1
12 A(A14)⊃R(F32(THM7,A13),A25(F32(THM7,A13),A14),A26(F32(THM7,A13),A14));INSERT
13 R(THM7,W,Y)∧R(A13,Y,X)⊃R(F32(THM7,A13),W,X);INSERT
14 R(W,X,F11(W,X));F1